A procedure for automatic proof nets construction
Identifieur interne : 00D705 ( Main/Exploration ); précédent : 00D704; suivant : 00D706A procedure for automatic proof nets construction
Auteurs : Didier Galmiche [France] ; Guy Perrier [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: In this paper, we consider the multiplicative fragment of linear logic (MLL) from an automated deduction point of view. Before to use this new logic to make logic programming or to program with proofs, a better comprehension of the proof construction process in this framework is necessary. We propose a new algorithm to construct automatically a proof net for a given sequent in MLL and its proofs of termination, correctness and completeness. It can be seen as an implementation oriented way to consider automated deduction in linear logic.
Url:
DOI: 10.1007/BFb0013047
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002A83
- to stream Istex, to step Curation: 002A46
- to stream Istex, to step Checkpoint: 003045
- to stream Main, to step Merge: 00DF82
- to stream Main, to step Curation: 00D705
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">A procedure for automatic proof nets construction</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B4E6F4380712799E76590A45B3227C72041BD9E0</idno><date when="1992" year="1992">1992</date><idno type="doi">10.1007/BFb0013047</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-RM9V8C83-3/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002A83</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002A83</idno><idno type="wicri:Area/Istex/Curation">002A46</idno><idno type="wicri:Area/Istex/Checkpoint">003045</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">003045</idno><idno type="wicri:doubleKey">0302-9743:1992:Galmiche D:a:procedure:for</idno><idno type="wicri:Area/Main/Merge">00DF82</idno><idno type="wicri:Area/Main/Curation">00D705</idno><idno type="wicri:Area/Main/Exploration">00D705</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">A procedure for automatic proof nets construction</title><author><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Lorraine Campus Scientifique, GRIN - CNRS - INRIA, B.P. 239, 54506, Vandœuvre-les-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Lorraine Campus Scientifique, GRIN - CNRS - INRIA, B.P. 239, 54506, Vandœuvre-les-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><title level="s" type="abbrev">Lect Notes Comput Sci</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: In this paper, we consider the multiplicative fragment of linear logic (MLL) from an automated deduction point of view. Before to use this new logic to make logic programming or to program with proofs, a better comprehension of the proof construction process in this framework is necessary. We propose a new algorithm to construct automatically a proof net for a given sequent in MLL and its proofs of termination, correctness and completeness. It can be seen as an implementation oriented way to consider automated deduction in linear logic.</div></front></TEI><affiliations><list><country><li>France</li></country><region><li>Grand Est</li><li>Lorraine (région)</li></region><settlement><li>Vandœuvre-lès-Nancy</li></settlement></list><tree><country name="France"><region name="Grand Est"><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name></region><name sortKey="Galmiche, Didier" sort="Galmiche, Didier" uniqKey="Galmiche D" first="Didier" last="Galmiche">Didier Galmiche</name><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name><name sortKey="Perrier, Guy" sort="Perrier, Guy" uniqKey="Perrier G" first="Guy" last="Perrier">Guy Perrier</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00D705 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00D705 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:B4E6F4380712799E76590A45B3227C72041BD9E0
|texte= A procedure for automatic proof nets construction
}}
| This area was generated with Dilib version V0.6.33. |  |